\begin{tabbing}
$\forall$\=$T$:Type, $t$:$T$, $l$:IdLnk, ${\it ds}_{1}$, ${\it ds}_{2}$:$x$:Id fp$\rightarrow$ Type, $P$:(State(${\it ds}_{1}$)$\rightarrow\mathbb{N}\rightarrow\mathbb{B}$), $Q$:(State(${\it ds}_{2}$)$\rightarrow\mathbb{N}\rightarrow\mathbb{B}$),\+
\\[0ex]$d_{1}$:($\forall$$s$:State(${\it ds}_{1}$). Dec($\exists$$n$:$\mathbb{N}$. ($\uparrow$($\neg_{b}$($P$($s$,$n$)))))),
\\[0ex]$d_{2}$:($\forall$$s$:State(${\it ds}_{2}$). Dec($\exists$$n$:$\mathbb{N}$. ($\uparrow$($\neg_{b}$($Q$($s$,$n$)))))), $f$:(State(${\it ds}_{1}$)$\rightarrow\mathbb{N}\rightarrow$$T$).
\-\\[0ex]Normal(${\it ds}_{1}$)
\\[0ex]$\Rightarrow$ Normal(${\it ds}_{2}$)
\\[0ex]$\Rightarrow$ ($\neg$(destination($l$) = source($l$) $\in$ Id))
\\[0ex]$\Rightarrow$ \=$\vdash$${\it es}$.@source($l$) state ${\it ds}_{1}$ \& ($\forall$$e$:E. (kind($e$) = rcv($l$,"tg") $\in$ Knd) $\Rightarrow$ (valtype($e$) $\subseteq$r $T$))\+
\\[0ex]\& @destination($l$) state ${\it ds}_{2}$
\\[0ex]\& ($\forall$$e$:E. (kind($e$) = rcv(lnk{-}inv($l$),"tg") $\in$ Knd) $\Rightarrow$ (valtype($e$) $\subseteq$r $\mathbb{Z}$))
\\[0ex]\& (\=@source($l$) discrete ${\it ds}_{1}$\+
\\[0ex]$\Rightarrow$ @destination($l$) discrete ${\it ds}_{2}$
\\[0ex]$\Rightarrow$ ($\forall$$k$:$\mathbb{N}$. @source($l$) stable $s$.$\uparrow$($P$($s$,$k$))  )
\\[0ex]$\Rightarrow$ ($\forall$$k$:$\mathbb{N}$. @destination($l$) stable $s$.$\uparrow$($Q$($s$,$k$))  )
\\[0ex]$\Rightarrow$ \=($\forall$$k$:$\mathbb{N}$.\+
\\[0ex]$\forall$$e$@source($l$).
\\[0ex]($\uparrow$($P$((discrete state after $e$),$k$)))
\\[0ex]$\Rightarrow$ $\exists$${\it e'}$@destination($l$).\=($\uparrow$($Q$((discrete state when ${\it e'}$),$k$)))\+
\\[0ex]$\vee$ ($\forall$$n$:$\mathbb{N}$. $\uparrow$($Q$((discrete state after ${\it e'}$),$n$))))
\-\-\\[0ex]$\Rightarrow$ \=($\forall$$e$:E.\+
\\[0ex](kind($e$) = rcv(lnk{-}inv($l$),"tg") $\in$ Knd)
\\[0ex]$\Rightarrow$ ($\forall$$k$:$\mathbb{N}$. ($k$ $<$ val($e$)) $\Rightarrow$ ($\uparrow$($P$((discrete state after $e$),$k$)))))
\-\\[0ex]$\Rightarrow$ \=($\forall$$k$:$\mathbb{N}$, $e$:E.\+
\\[0ex](kind($e$) = rcv($l$,"tg") $\in$ Knd)
\\[0ex]$\Rightarrow$ (val($e$) = $f$((state when sender($e$)),$k$) $\in$ $T$)
\\[0ex]$\Rightarrow$ ($\uparrow$($Q$((discrete state after $e$),$k$))))
\-\\[0ex]$\Rightarrow$ $\exists$$e$@destination($l$).True
\\[0ex]$\Rightarrow$ \=($\forall$$k$:$\mathbb{N}$.\+
\\[0ex]$\exists$$e$@destination($l$).\=($\forall$$n$:\{0..$k$$^{-}$\}. $\uparrow$($Q$((discrete state when $e$),$n$)))\+
\\[0ex]$\vee$ ($\forall$$n$:$\mathbb{N}$. $\uparrow$($Q$((discrete state after $e$),$n$)))))
\-\-\-\-
\end{tabbing}